$\forall$$A$, $B$, $C$:Type. $A$ $\sim$ $B$ $\Rightarrow$ :$C$ $\times$ $A$ $\sim$ :$C$ $\times$ $B$